package xyz.scootaloo.code.draft.discrete

import xyz.scootaloo.code.common.copy

/**
 * 命题公式计算器
 *
 * 1. 根据字符串格式的命题公式, 生成语法树
 * 2. 然后应用符号运算规则, 得到结果
 *
 * @author flutterdash@qq.com
 * @since 2021/10/7 22:09
 */

fun main() {
    expr("(!p&q)->!r").show()
    expr("(p|!p)<->(q|!q)").show()
    expr("!(p->q)&q&r").show()
    expr("!q or p").show()
}

/**
 * 输入表达式, 返回语法树根节点
 *
 * 由于一些命题公式的符号不能用键盘输入, 例如取反操作符"┐",
 * 所以在程序设计的时候, 用其他关键字(例如 not)来代替这些不能由键盘输入的符号
 *
 * 支持的符号
 * ┐ not !     取反
 * and &       合取
 * or |        汲取
 * ( )         括号
 * -> <->      蕴含 等价
 * xor         异或
 *
 * 合法输入:
 *      "pandqorrorc" 变量个操作符之间的空格不是必须的, 左边的表达式和 "p and q or r or c" 等价
 *      上面的表达式也可以写成 "p&q|r|c"
 * 其他示例:
 *      "(!p and q) -> !r"
 *      "(p and !q)<->(q and !q)"
 *      "!(p<->q)and q and r"
 *      "(!p or q) and ((p and r)->p)"
 *
 * 不合法输入:
 *      "!p and q)->!r"
 *               ^   唐突的右括号
 *      "(!xx&c) xor c"
 *         ^^   一般命题变量是一个小写英文字母, 有不合规范的命题变量, 会予以提示, 但不影响公式计算
 *      "and((a|b)->)and!"
 *       ^^^      ^^    ^   箭头指向的三个位置缺少左值或右值, 这样的公式是不完整的, 也不能计算
 *
 *      假如输入的公式包含这几种情况, 会在控制台看到提示
 *
 * 输出:
 *      输出的是语法树的根节点
 *      当输入是 "(a->b)<->!(b->c)", 会生成如下树状结构
 *
 *              <-> 被返回的节点, 表达式节点的结果是 左子树 和 右子树 进行 操作符运算的结果
 *             /   \
 *            ->    !
 *           /  \    \
 *          a    b   ->
 *                  /  \
 *                 b    c
 *
 * @param expr 表达式
 * @param ctx  上下文; 上下文中存储了命题变元, 以及命题变元的真值; 可以根据需要注入
 * @return     假如表达式格式正确, 没有缺失的结构, 则 [ExpressionHolder.success] 为true, 否则返回的表达式不能进行计算
 */
fun expr(
    expr: String, ctx: LocalContext = ctx()
): ExpressionHolder {
    val segments = parse(StringBuilder(expr).append(' '))
    var resolving = integrityAnalysis(expr, segments)
    if (errorHandle(expr, resolving))
        return ExpressionHolder(false)

    val root = buildSyntaxTree(segments, ctx)
    resolving = checkIntegrity(root, ArrayList())
    if (errorHandle(expr, resolving))
        return ExpressionHolder(false)

    return ExpressionHolder(true, expr, root, ctx)
}

/**
 * 解析原始表达式, 将表达式拆分为符号组成的列表
 */
private fun parse(exp: StringBuilder): List<SymbolDesc> {
    val stopSigns = arrayOf('(', ' ', ')')
    val presets = GlobalContext.presetSymbols
    val res = ArrayList<SymbolDesc>()
    val buff = StringBuilder()

    fun storageToRes(syb: String) {
        res.add(SymbolDesc(syb))
    }

    fun storageAndClearBuff() {
        if (buff.isNotEmpty())
            storageToRes(buff.toString())
        buff.clear()
    }

    fun parse2(content: String, symbol: String, start: Int): String {
        val prefix = content.substring(0, start)
        var infix = content.substring(start)
        val postfix = infix.substring(symbol.length)
        infix = infix.substring(0, symbol.length)

        if (prefix.isNotEmpty()) storageToRes(prefix)
        if (infix.isNotEmpty()) storageToRes(infix)

        return postfix
    }

    fun parse1(content: String) {
        if (content.isEmpty())
            return

        var mostNearly = Int.MAX_VALUE
        var mostNearlySymbol = ""
        for (preset in presets) {
            val distance = content.indexOf(preset)
            if (distance != -1 && distance < mostNearly) {
                mostNearly = distance
                mostNearlySymbol = preset
            }
        }

        if (mostNearly != Int.MAX_VALUE) {
            return parse1(parse2(content, mostNearlySymbol, mostNearly))
        } else {
            storageToRes(content)
            buff.clear()
        }
    }

    fun parse0() {
        if (buff.length <= 1)
            return storageAndClearBuff()
        val content = buff.toString()
        buff.clear()
        parse1(content)
    }

    for (idx in exp.indices) {
        val ch = exp[idx]
        if (ch in stopSigns) {
            parse0()
            if (ch != ' ')
                storageToRes(ch.toString())
        } else {
            buff.append(ch)
        }
    }

    return res
}

/**
 * 完整性分析
 * 检查是否有不能处理或不符合规范的符号, 假如有, 报错或警告.
 * 检查括号是否完整, 即每个左括号有右括号对应, 是否存在未配对的括号
 *
 * !只能处理圆括号, 不能处理其他类型的括号
 */
private fun integrityAnalysis(
    rawExpr: String, symbols: List<SymbolDesc>
): List<ParseResult> {
    // 标记每个符号的位置
    fun completeSymbolDesc(start: Int = 0, index: Int = 0): ParseResult {
        if (index == symbols.size || start >= rawExpr.length)
            return ParseResult()
        val current = symbols[index]
        val appear = rawExpr.indexOf(current.symbol, start)
        return if (appear >= 0) {
            current.position = appear
            completeSymbolDesc((appear + current.symbol.length), index + 1)
        } else {
            ParseResult(false, message = "分析符号出现位置时遇到问题", isError = true)
        }
    }

    // 检查所有括号是否可以配对
    fun checkParentheses(): ParseResult {
        var left = 0
        var lastLeft = 0
        for (idx in rawExpr.indices) {
            val ch = rawExpr[idx]
            if (ch != '(' && ch != ')')
                continue
            if (ch == '(') {
                left++
                lastLeft = idx
            } else {
                if (left <= 0) {
                    return ParseResult(
                        false,
                        idx, idx, idx, "缺少左括号", isError = true
                    )
                } else {
                    left--
                }
            }
        }
        if (left > 0)
            return ParseResult(
                false,
                lastLeft, lastLeft, rawExpr.length - 1, "缺少右括号",
                isError = true
            )
        return ParseResult()
    }

    // 检查所有变量名是否符合规范
    fun checkVariableNaming(): List<ParseResult> {
        val warnings = ArrayList<ParseResult>()
        for (symbol in symbols) {
            if (!GlobalContext.presetSymbols.contains(symbol.symbol)) {
                if (symbol.symbol.length > 1) {
                    warnings.add(
                        ParseResult(
                            false,
                            symbol.position, symbol.position,
                            (symbol.position + symbol.symbol.length - 1),
                            "符号`${symbol.symbol}`已被处理为变量"
                        )
                    )
                }
            }
        }
        return warnings
    }

    return ArrayList<ParseResult>().apply {
        addError(completeSymbolDesc())
        addError(checkParentheses())
        addAllError(checkVariableNaming())
    }
}

/**
 * 构建语法树
 *
 * 表达式的填充标记:
 *      1: 需要填充左值
 *      2: 需要填充右值
 *      3: 已经是完整的表达式了
 * 转换流程 3 -> 1 -> 2 -> 3 -> 1 -> 2 ... ...
 * - 符号标记由操作符返回, and操作符需要左值和右值所以返回1, not操作符只需要右值, 所以not操作符返回2, ...
 * - 实际情况下, 表达式从左向右读取, 左值优先于操作符被处理, 所以status只有状态2和3
 *
 * 1. 假如读取到一个左括号, 将括号范围内的表达式从待处理的符号列表中删除, 同时将括号内的表达式处理成 [Expression] 对象返回
 * 2. 假如读取到一个操作符, 将上一个表达式做为当前操作符的左值, 然后修改符号标记, 最后将当前操作符做为当前表达式
 *      2.1 读取右边最近的一个完全表达式, 赋为右值
 * 3. 假如读取到一个变量, 检查当前的符号标记, 假如为1或者2, 将当前变量赋值为当前表达式的左值或右值, 否则将当前变量做为当前表达式
 * 4. 读取完所有的符号列表, 将当前表达式返回
 *
 * @return 返回语法树的根节点
 */
private fun buildSyntaxTree(
    symbols: List<SymbolDesc>, context: LocalContext
): Expression = buildSyntaxTreeInScope(symbols.copy(), context)

private fun buildSyntaxTreeInScope(
    rest: MutableList<SymbolDesc>, context: LocalContext
): Expression {
    var status = 3
    var topNode: Expression = EmptyExpr

    /**
     * @param down 标记传进来的是一个括号里的表达式
     */
    fun updateStatusAndPlaceExpr(expr: Expression, down: Boolean = false) {
        when (status) { // status 代表上一个表达式的状态
            1 -> topNode.leftExpr = expr
            2 -> {
                topNode.rightExpr = expr
                /**
                 * 处理运算符符后面的单目运算符, 满足条件:
                 * 1. 参数表达式 [expr] 不是括号内的表达式
                 * 2. 当前顶层表达式是操作符, 并且参数表达式也是操作符
                 * then: 将下一个变量表达式提取, 并做为参数表达式的右值
                 *
                 * 下面的表达式符合这种情况
                 * (1) p->!(a<->b)     (2) (a->b)&!b     <1>.->和!都是操作符, 所以!连带右边最近的完整表达式做为右值
                 *      ^^________               ^__     <2>.&和!都是操作符, 和(1)同理
                 *        ->                   &
                 *       /  \                /  \
                 *      p    !              ->   !
                 *            \            /  \   \
                 *            <->         a    b   b
                 *           /  \
                 *          a    b
                 */
                if (!down && topNode is OperatorExpr && expr is OperatorExpr) {
                    val rightValue = extractNextExpression(rest, context)
                    expr.rightExpr = rightValue
                }
            }
            3 -> {
                if (topNode != EmptyExpr)
                    expr.leftExpr = topNode
                topNode = expr
                status = expr.operator.type
            }
        }

        // 更新当前表达式的状态
        status++
        if (down) // 括号内的表达式是完整不能分割的, 直接进入下一轮转换
            status = 3
    }

    while (rest.isNotEmpty()) {
        val syb = rest.removeAt(0)
        if (syb.symbol == "(") { // 括号内的表达式做为一个整体
            val exprInParentheses = buildSyntaxTreeInParentheses(rest, context)
            updateStatusAndPlaceExpr(exprInParentheses, true)
        } else if (GlobalContext.isKeyWord(syb.symbol)) {
            val operatorExpr = OperatorExpr(GlobalContext.getOperator(syb), syb)
            updateStatusAndPlaceExpr(operatorExpr)
        } else {
            val variate = syb.symbol
            context.registerVariate(variate)
            updateStatusAndPlaceExpr(VariateExpr(syb))
        }
    }

    return topNode
}

private fun extractNextExpression(
    rest: MutableList<SymbolDesc>, context: LocalContext
): Expression {
    if (rest.isEmpty()) return EmptyExpr
    val syb = rest.removeAt(0)
    return if (GlobalContext.isKeyWord(syb.symbol)) {
        val expr = OperatorExpr(GlobalContext.getOperator(syb), syb)
        expr.rightExpr = extractNextExpression(rest, context)
        expr
    } else if (syb.symbol == "(") {
        buildSyntaxTreeInParentheses(rest, context)
    } else {
        context.registerVariate(syb.symbol)
        VariateExpr(syb)
    }
}

/**
 * 将一对括号内的表达式构建为语法树
 *
 * expr = "((a->b)^(a->c))"
 *         ^
 *        remove
 * input "(a->b)^(a->c))"
 * output
 *         ^
 *      /    \
 *     ->    ->
 *    /  \   /  \
 *   a    b a    c
 */
private fun buildSyntaxTreeInParentheses(
    ref: MutableList<SymbolDesc>, context: LocalContext
): Expression {
    var left = 1
    val rest = ArrayList<SymbolDesc>()
    while (true) {
        val syb = ref.removeAt(0)
        when (syb.symbol) {
            "(" -> left++
            ")" -> left--
        }

        if (left == 0) {
            break
        } else {
            rest.add(syb)
        }
    }
    return buildSyntaxTreeInScope(rest, context)
}

private fun checkIntegrity(
    expr: Expression, collector: MutableList<ParseResult>
): List<ParseResult> {
    if (expr.leftExpr != EmptyExpr)
        checkIntegrity(expr.leftExpr, collector)
    collector.addAllError(expr.checkIntegrity())
    if (expr.rightExpr != EmptyExpr)
        checkIntegrity(expr.rightExpr, collector)
    return collector
}

/**
 * 将错误信息显示在控制台上
 *
 * @return 决定是否退出余下的分析过程
 */
private fun errorHandle(expr: String, errors: List<ParseResult>): Boolean {
    if (errors.isEmpty()) return false

    val line2 = CharArray(expr.length + 1) { ' ' }
    val line3 = CharArray(expr.length + 1) { ' ' }
    val comment = StringBuilder()

    class OrderedStruct(
        val point: Int,
        val error: ParseResult,
        var id: Int = 0
    )

    val orderedList = ArrayList<OrderedStruct>()

    var needExit = false

    for (error in errors) {
        if (error.isError) needExit = true

        for (idx in error.left..error.right) {
            line2[idx] = '~'
        }

        orderedList.add(OrderedStruct(error.point, error))
    }

    orderedList.sortBy { it.point }
    for (idx in orderedList.indices) {
        orderedList[idx].id = idx + 1
        line3[orderedList[idx].point] = '0' + orderedList[idx].id
    }

    val retract = "    $"
    for (warning in orderedList) {
        comment.append(retract).append(warning.id)
        comment.append(": ")
        if (warning.error.isError)
            comment.append("[error]")
        else
            comment.append("[warning]")
        comment.append(' ').append(warning.error.message).append('\n')
    }

    println(expr)
    println(line2)
    println(line3)
    println(comment)

    return if (needExit) {
        println("\$分析中止$\n")
        true
    } else {
        false
    }
}

private fun MutableList<ParseResult>.addError(result: ParseResult) {
    if (!result.success)
        this.add(result)
}

private fun MutableList<ParseResult>.addAllError(results: Collection<ParseResult>) {
    for (result in results)
        addError(result)
}

private fun ctx(): LocalContext = LocalContext()

data class SymbolDesc(
    val symbol: String,
    var position: Int = 0
) {
    override fun toString(): String {
        return "['$symbol', $position]"
    }
}

class ParseResult(
    val success: Boolean = true,
    val point: Int = 0,
    val left: Int = 0,
    val right: Int = 0,
    val message: String = "",
    val isError: Boolean = false
)

abstract class Expression(
    val symbol: SymbolDesc
) {
    var leftExpr: Expression = EmptyExpr
    var rightExpr: Expression = EmptyExpr

    var operator: Operator = EmptyOperator

    abstract fun eval(ctx: LocalContext): Boolean

    open fun checkIntegrity(): List<ParseResult> = operator.checkIntegrity(this)

    override fun toString(): String = symbol.symbol
}

object EmptyExpr : Expression(SymbolDesc("", -1)) {
    override fun eval(ctx: LocalContext): Boolean {
        throw RuntimeException("空表达式不能被执行")
    }

    override fun checkIntegrity(): List<ParseResult> = emptyList()
    override fun toString(): String = "#"
}

class VariateExpr(symbol: SymbolDesc) : Expression(symbol) {
    override fun eval(ctx: LocalContext): Boolean =
        ctx.getVariateValue(symbol.symbol)
}

class OperatorExpr(operator: Operator, symbol: SymbolDesc) : Expression(symbol) {
    init {
        this.operator = operator
    }

    override fun eval(ctx: LocalContext): Boolean = operator.eval(this, ctx)
}

abstract class Operator(
    vararg val accept: String
) {
    open val type = 1

    open fun checkIntegrity(expr: Expression): List<ParseResult> = listOf(
        LackChecker.LeftExprChecker.check(expr),
        LackChecker.RightExprChecker.check(expr)
    )

    abstract fun eval(expr: Expression, ctx: LocalContext): Boolean
}

object EmptyOperator : Operator() {
    override val type: Int = 2

    override fun checkIntegrity(expr: Expression): List<ParseResult> = emptyList()
    override fun eval(expr: Expression, ctx: LocalContext): Boolean {
        throw RuntimeException("空操作符不能被运算")
    }
}

object NotOperator : Operator("not", "!", "┐") {
    override val type: Int = 1

    override fun eval(expr: Expression, ctx: LocalContext): Boolean =
        !expr.rightExpr.eval(ctx)

    override fun checkIntegrity(expr: Expression): List<ParseResult> =
        listOf(LackChecker.RightExprChecker.check(expr))
}

object ContainOperator : Operator("->") {
    override fun eval(expr: Expression, ctx: LocalContext): Boolean {
        val lv = expr.leftExpr.eval(ctx)
        return if (!lv) true else expr.rightExpr.eval(ctx)
    }
}

object AndOperator : Operator("and", "&") {
    override fun eval(expr: Expression, ctx: LocalContext): Boolean =
        expr.leftExpr.eval(ctx) && expr.rightExpr.eval(ctx)
}

object OrOperator : Operator("or", "|", "^") {
    override fun eval(expr: Expression, ctx: LocalContext): Boolean =
        expr.leftExpr.eval(ctx) || expr.rightExpr.eval(ctx)
}

object XorOperator : Operator("xor") {
    override fun eval(expr: Expression, ctx: LocalContext): Boolean =
        expr.leftExpr.eval(ctx) != expr.rightExpr.eval(ctx)
}

object EqualOperator : Operator("<->") {
    override fun eval(expr: Expression, ctx: LocalContext): Boolean =
        expr.leftExpr.eval(ctx) == expr.rightExpr.eval(ctx)
}

sealed class LackChecker {
    abstract fun check(expr: Expression): ParseResult

    protected fun failureResultBuild(symbol: SymbolDesc, msg: String): ParseResult {
        return ParseResult(
            success = false,
            point = symbol.position,
            left = symbol.position,
            right = symbol.position + symbol.symbol.length - 1,
            msg,
            isError = true
        )
    }

    object LeftExprChecker : LackChecker() {
        override fun check(expr: Expression): ParseResult =
            if (expr.leftExpr == EmptyExpr)
                failureResultBuild(expr.symbol, "缺少左值")
            else ParseResult()
    }

    object RightExprChecker : LackChecker() {
        override fun check(expr: Expression): ParseResult =
            if (expr.rightExpr == EmptyExpr)
                failureResultBuild(expr.symbol, "缺少右值")
            else ParseResult()
    }
}

data class ExpressionHolder(
    val success: Boolean,
    val exprStr: String = "",
    val expression: Expression = EmptyExpr,
    val localContext: LocalContext = LocalContext()
)

private object GlobalContext {
    val presetOperators: List<Operator> = listOf(
        NotOperator, ContainOperator, AndOperator, OrOperator, EqualOperator, XorOperator
    )
    val presetSymbols: List<String> = presetSymbols()
    val operatorMapper: Map<String, Operator> = operatorMapper()

    fun isKeyWord(symbol: String): Boolean = presetSymbols.contains(symbol)

    fun getOperator(symbol: SymbolDesc): Operator = operatorMapper[symbol.symbol]!!

    private fun operatorMapper(): Map<String, Operator> {
        return HashMap<String, Operator>().apply map@{
            for (preset in presetOperators) {
                for (accept in preset.accept) {
                    this@map[accept] = preset
                }
            }
        }
    }

    private fun presetSymbols(): List<String> =
        presetOperators.flatMap { expr -> expr.accept.asList() }
}

class LocalContext(
    private val variateTable: MutableList<String> = ArrayList(),
    private var variateMap: HashMap<String, Boolean> = HashMap()
) {
    fun getVariateValue(variate: String): Boolean = variateMap[variate]!!
    fun registerVariate(variate: String) {
        if (!variateMap.contains(variate)) {
            variateTable.add(variate)
            variateMap[variate] = true
        }
    }

    internal fun variates(): MutableList<String> = variateTable.copy()
    internal fun refresh(block: HashMap<String, Boolean>.() -> Unit) =
        variateMap.block()
}
